Issue2828.agda:12,9-11
⊤ !=< X
when checking that the expression tt has type X
